Nuprl Lemma : Q-R-pre-preserving_wf
11,40
postcript
pdf
es
:ES,
P
:(E
),
Q
,
R
:(E
E
),
f
:({
e
:E|
P
(
e
)}
E).
f
is
Q
-
R
-pre-preserving on
P
latex
Definitions
ES
,
t
T
,
Type
,
,
x
:
A
.
B
(
x
)
,
E
,
x
:
A
B
(
x
)
,
f
(
a
)
,
{
x
:
A
|
B
(
x
)}
,
P
Q
,
f
is
Q
-
R
-pre-preserving on
P
Lemmas
es-E
wf
,
event
system
wf
origin
es:ES, P:(E
), Q, R:(EE), f:({e:E| P(e)} E). f is Q-R-pre-preserving on P 
es:ES, P:(E), Q, R:(EE), f:({e:E| P(e)} E). f is Q-R-pre-preserving on P Tx:A. B(x)B(x)
Q